Automating and scaling pre-silicon functional verification of state-of-the-art hardware designs, such as microprocessors and microcontrollers, presents many challenges. For example, the use of non-deterministic elements, commonly signified by X, for logic minimization and partial reset of large datapath registers can be effective in reducing the power and area consumption of certain logic in the chip. In certain cases, X's are also inserted to test hypothetical scenarios for improving coverage and other aspects of the design. However, the use of X's introduces verification challenges if not coupled with systematic methodologies and tools that can show that the non-determinism introduced by the X's does not propagate to the outputs of the design.
Sequential X refers herein to the problem of deciding if certain sampling points, including outputs, of an RTL design are deterministic, even with the presence of X's inside the design—referring to detecting the presence of Don't Cares, or X's, on these points. In this disclosure, a formal expression of the Sequential X problem is presented and algorithms which provide varying checking completeness are examined. Reveal-SEQX, an implementation of a Sequential X consistency checker which uses the Reveal model checker and a specialized correctness generator is also described. Further description of the Reveal model checker may be found in Automatic Formal Verification of Control Logic in Hardware Designs, Z. Andraus, Ph.D Dissertation, University of Michigan, April 2009. Reveal-SEQX is applied on a number of publicly available designs to reason about their output Don't Cares. Lastly, it is shown how the methodology and tool are used to avoid “good” X's appearing as false alarms, and to prove that the design is free of output X's.
This section provides background information related to the present disclosure which is not necessarily prior art.